package com.googlecode.kipler.satisfiability.interpolation.rule;

import java.util.Stack;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.rule.trace.RuleTrace;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;

public class FlatTracingInterpolantCalculation {

	private WorldConstraintSystem wcs;

	private ConceptAssertion previousInterpolant;

	public WorldConstraintSystem getWcs() {
		return wcs;
	}

	public void setWcs(WorldConstraintSystem wcs) {
		this.wcs = wcs;
	}

	public ConceptAssertion getPreviousInterpolant() {
		return previousInterpolant;
	}

	public void setPreviousInterpolant(ConceptAssertion previousInterpolant) {
		this.previousInterpolant = previousInterpolant;
	}

	public ConceptAssertion apply() {
		Stack<RuleTrace> tracing = ((BasicWcsInterpolationData) getWcs()
				.getData()).getRuleTracing();
		while (!tracing.empty()) {
			RuleTrace trace = tracing.pop();
			InterpolantRule iRule = null;
			switch (trace.getType()) {
			case CLASH:
				iRule = new ClashInterpolantRule();
				break;
			case SOME_VALUES:
				iRule = new SomeValuesInterpolantRule();
				break;
			}
			if (iRule != null) {
				iRule.setCondition(trace.getConstraints());
				iRule.addPreviousInterpolant(previousInterpolant);
				iRule.setWcs(getWcs());
				previousInterpolant = iRule.apply();
			}
		}
		return previousInterpolant;
	}
}
